\begin{problema}{usuariosEficientesT}{t: Trivia}{[Usuario]}
	\asegura[puedeNoHaberNadie]{\longitud {result}==0 \implica \longitud{participantes(t)} == 0}
	\asegura[sonParticipantes]{(\forall u \selec result)u \in particpantes(t)}
	\asegura[noSobran]{(\forall u \selec result)esEficiente(t,u)}
	\asegura[noFaltan]{(\forall u \selec participantes(t),esEficiente(t,u)) u \in result}
	\asegura{sinRepetidos(result)}
\end{problema}	
	
	\medskip

\begin{aux}{esEficiente}{t:Trivia, u:Usuario}{Bool}{
	(\forall h \selec participantes(t)) puntajeAcumulado(t,u) \geq puntajeAcumulado(t,h) \\
	\ylogico (\forall h \selec participantes(t), puntajeAcumulado(t,u) == puntajeAcumulado (t,h)) \\
	cantidadMensajes(t,u) \leq cantidadMensajes(t,h))}
\end{aux}